\begin{tabbing}
PossibleWorld($D$;$w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=FairFifo\+
\\[0ex]\& (\=($\forall$$i$, $x$:Id. vartype($i$;$x$) $\subseteq$r M($i$).ds($x$))\+
\\[0ex]c$\wedge$ ($\forall$$i$:Id, $a$:Action($i$). ($\neg$($\uparrow$isnull($a$))) $\Rightarrow$ (valtype($i$;$a$) $\subseteq$r M($i$).da(kind($a$))))
\\[0ex]c$\wedge$ ($\forall$$l$:IdLnk, ${\it tg}$:Id. ($w$.M($l$,${\it tg}$)) $\subseteq$r M(source($l$)).da(rcv($l$,${\it tg}$)))
\\[0ex]c$\wedge$ ($\forall$$i$, $x$:Id. M($i$).init($x$,s($i$;0).$x$))
\\[0ex]c$\wedge$ \=($\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$isnull(a($i$;$t$))))
\\[0ex]$\Rightarrow$ \=((\=($\uparrow$islocal(kind(a($i$;$t$))))\+\+
\\[0ex]$\Rightarrow$ \=(M($i$).pre(act(kind(a($i$;$t$))),read{-}state($\lambda$$x$.s($i$;$t$).$x$))\+
\\[0ex]\& ma{-}random(\=M($i$);\+
\\[0ex]valtype($i$;a($i$;$t$));
\\[0ex]val(a($i$;$t$));$i$;act(kind(a($i$;$t$)));w{-}knum($w$;$i$;kind(a($i$;$t$));$t$))))
\-\-\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]M($i$).ef(kind(a($i$;$t$)),
\\[0ex]$x$,read{-}state($\lambda$$x$.s($i$;$t$).$x$),val(a($i$;$t$)),$\lambda$$q$.s($i$;$t$+1).$x$($q$ {-} 1)))
\-\\[0ex]\& (\=$\forall$$l$:IdLnk.\+
\\[0ex]M($i$).send(kind(a($i$;$t$));
\\[0ex]$l$;read{-}state($\lambda$$x$.s($i$;$t$).$x$);val(a($i$;$t$));withlnk($l$;m($i$;$t$));$i$))
\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]($\neg$M($i$).frame(kind(a($i$;$t$)) affects $x$))
\\[0ex]$\Rightarrow$ ($\forall$$r$:$\mathbb{Q}$. s($i$;$t$).$x$($r$ + 1) = s($i$;$t$+1).$x$($r$)))
\-\\[0ex]\& (\=$\forall$$l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]($\neg$M($i$).sframe(kind(a($i$;$t$)) sends $<$$l$,${\it tg}$$>$))
\\[0ex]$\Rightarrow$ (w{-}tagged(${\it tg}$;onlnk($l$;m($i$;$t$))) = []))))
\-\-\-\\[0ex]c$\wedge$ \=((\=$\forall$$i$, $a$:Id, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$\=${\it t'}$:$\mathbb{N}$\+
\\[0ex](($t$ $\leq$ ${\it t'}$)
\\[0ex]\& (\=(($\neg$($\uparrow$isnull(a($i$;${\it t'}$)))) c$\wedge$ (kind(a($i$;${\it t'}$)) = locl($a$)))\+
\\[0ex]$\vee$ ($\neg$$a$ declared in M($i$))
\\[0ex]$\vee$ unsolvable M($i$).pre($a$,read{-}state($\lambda$$x$.s($i$;${\it t'}$).$x$)))))
\-\-\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$isnull(a($i$;$t$))))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id.\+
\\[0ex]($\neg$M($i$).aframe(kind(a($i$;$t$)) affects $x$))
\\[0ex]$\Rightarrow$ ($\forall$$r$:$\mathbb{Q}$. s($i$;$t$).$x$($r$ + 1) = s($i$;$t$+1).$x$($r$))))
\-\-\\[0ex]\& (\=$\forall$$i$, $x$:Id, $k$:Knd.\+
\\[0ex]($\neg$M($i$).rframe($k$ reads $x$)) $\Rightarrow$ w{-}machine{-}independent($w$;$i$;$k$;$x$))
\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\neg$($\uparrow$isnull(a($i$;$t$))))
\\[0ex]$\Rightarrow$ \=($\forall$$l$:IdLnk.\+
\\[0ex]($\neg$M($i$).bframe(kind(a($i$;$t$)) sends on $l$)) $\Rightarrow$ (onlnk($l$;m($i$;$t$)) = [])))))
\-\-\-\-\-
\end{tabbing}